ds, ds':ltg:Id fp Type. ds  ds'  State(ds')  State(ds) 

latex

Definitions	f  g, IdDeq, a:A fp B(a), x. t(x), Id, S  T, State(ds), t  T, x:A. B(x), P  Q
Lemmas	ma-state-subtype, ma-state wf, Id wf, fpf wf, id-deq wf, fpf-sub wf